(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
m2(S(0), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0, b, res, True) → False
m3(S(0), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0, b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0)), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0, y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0) → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0, False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
Rewrite Strategy: INNERMOST
(1) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
m2/2
m3/1
m3/2
m3/3
l8/2
l8/4
l8/5
l5/2
l5/3
l5/4
e4/0
e4/1
e4/2
e2/2
l15/0
l15/2
l15/3
l15/5
l16/0
l16/1
l16/3
l16/4
l16/5
l13/0
l13/2
l13/3
l13/5
m4/2
m4/3
m5/0
m5/1
m5/3
l10/2
l10/3
l10/4
l10/5
l7/2
l7/3
l7/4
l7/5
l2/3
l2/4
l3/2
l3/3
l3/4
l3/5
l11/2
l11/3
l11/4
l14/2
l14/3
l14/4
l14/5
l12/2
l12/3
l12/4
l12/5
e3/2
e3/3
m1/2
m1/3
l9/1
l9/2
l9/3
l9/4
l9/5
l6/0
l6/1
l6/2
l6/3
l6/4
l6/5
l4/2
l4/3
l4/4
l4/5
l1/3
l1/4
l1/5
e7/0
e7/1
e7/2
e7/3
e6/0
e6/1
e6/2
e6/3
e5/0
e5/1
e5/2
e5/3
e1/2
e1/3
e8/0
e8/1
e8/3
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
m2(S(0), b, True) → False
m2(S(S(x)), b, True) → True
m2(0, b, True) → False
m3(S(0)) → False
m3(S(S(x))) → True
m3(0) → False
l8(res, y, True) → res
l5(x, y, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(False) → False
e4(True) → True
e2(a, b, False) → False
l15(y, False) → l16(gcd(y, 0))
l15(y, True) → l16(gcd(y, S(0)))
l13(y, False) → l16(gcd(0, y))
l13(y, True) → l16(gcd(S(0), y))
m4(S(x'), S(x)) → m5(monus(x', x))
m2(a, b, False) → m4(a, b)
l8(x, y, False) → l10(x, y)
l5(x, y, False) → l7(x, y)
l2(x, y, res, False) → l3(x, y)
l2(x, y, res, True) → res
l11(x, y, False) → l14(x, y)
l11(x, y, True) → l12(x, y)
help1(0) → False
e2(a, b, True) → e3(a, b)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x) → m2(a, x, False)
l9(res) → res
l6 → 0
l4(x', x) → l5(x', x, False)
l1(x, y, res) → l2(x, y, res, False)
e7 → False
e6 → False
e5 → True
monus(a, b) → m1(a, b)
m5(res) → res
l7(x, y) → l8(x, y, equal0(x, y))
l3(x, y) → l4(x, y)
l16(res) → res
l14(x, y) → l15(y, monus(x, y))
l12(x, y) → l13(y, monus(x, y))
l10(x, y) → l11(x, y, <(x, y))
gcd(x, y) → l1(x, y, 0)
equal0(a, b) → e1(a, b)
e8(res) → res
e3(a, b) → e4(<(b, a))
e1(a, b) → e2(a, b, <(a, b))
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
Rewrite Strategy: INNERMOST
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
m4(S(x'), S(x)) →+ m5(m4(x', x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x' / S(x'), x / S(x)].
The result substitution is [ ].
(4) BOUNDS(n^1, INF)